Nuprl Lemma : s-dsys-sub-s-dsys
0,22
postcript
pdf
A
,
B
:System. (
i
:Id.
A
(
i
)
B
(
i
))
s-dsys(
A
)
s-dsys(
B
)
latex
Definitions
s-dsys(
M
)
,
M(
i
)
,
System
,
P
Q
,
D1
D2
,
Prop
,
M1
M2
,
MsgA
,
Id
,
Feasible(
M
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
ma-feasible
wf
,
Id
wf
,
msga
wf
,
ma-sub
wf
origin
A, B:System. (i:Id. A(i) 
B(i)) 
s-dsys(A) s-dsys(B) A, B:System. (i:Id. A(i) B(i)) s-dsys(A) s-dsys(B) Q D2 M2x:A. B(x)
T